package kodkod.ast.visitor.graph;

import java.io.*;
import java.util.*;

import kodkod.analysis.ast.GraphVisitor;
import kodkod.ast.*;

public class GraphVisitorDOT extends GraphVisitor {
	StringBuffer nodes = new StringBuffer();
	StringBuffer edges = new StringBuffer();
	
	ArrayList<Node> leafNodes = new ArrayList<Node>();
	ArrayList<ArrayList<Node>> rankGroups = new ArrayList<ArrayList<Node>>();
	
	File graphFile = null;
	BufferedWriter writer = null;
	
	boolean do_ranking = false;
	
	public GraphVisitorDOT() {
		try {
			graphFile = File.createTempFile("Graph", ".dot");
			writer = new BufferedWriter(new FileWriter(graphFile));
		} catch (IOException e) {
			e.printStackTrace();
		}
	}
	
	public GraphVisitorDOT(File file) {
		try {
			graphFile = file;
			writer = new BufferedWriter(new FileWriter(graphFile));
		} catch (IOException e) {
			e.printStackTrace();
		}		
	}
	
	public void finalize() {
		try {
			writer.close();
		} catch (IOException e) {
			e.printStackTrace();
		}
	}
		
	public void flush() {
		try {
			writer.write("digraph AST {\n");
			writer.write("ranksep=1.0\n");
			writer.write(nodes.toString());
			writer.write(edges.toString());
			
			if (do_ranking) {
				writer.write("{rank=sink;");
				for(Node node : leafNodes) if (node instanceof Relation) {
					writer.write("N"+getNodeId(node)+" ");
				}
				writer.write("}\n");
				
				writer.write("{rank=same;");
				for(Node node : leafNodes) if (node instanceof Variable) {
					writer.write("N"+getNodeId(node)+" ");
				}
				writer.write("}\n");
				
				for (ArrayList<Node> rankGroup : rankGroups) {
					writer.write("{rank=same;");
					for(Node node : rankGroup) {
						writer.write("N"+getNodeId(node)+" ");
					}
					writer.write("}\n");
				}
			}
			
			writer.write("}\n");
			
			writer.close();
		} catch (IOException e) {
			e.printStackTrace();
		}
	}
	
	@Override
	protected void newEdge(Node parent, Node child) {
		int parentId = getNodeId(parent);
		int childId = getNodeId(child);
		edges.append("N"+parentId+"->N"+childId+" [dir=back]\n");
	}
	
	@Override
	protected void newNode(Node node) {
		int id = getNodeId(node);
		nodes.append("N"+id+" [");
		nodes.append("label=\""+getNodeName(node)+"\"");
		if (node instanceof Formula) {
			nodes.append(", shape=triangle");
		} else if (node instanceof Expression) {
			if (node instanceof LeafExpression) {
				if (node instanceof Variable) {
					nodes.append(", shape=ellipse");
				} else {
					nodes.append(", shape=box");
				}
			} else if (node instanceof BinaryExpression) {
				nodes.append(", shape=Mdiamond");
			} else {
				nodes.append(", shape=diamond");
			}
		} else if (node instanceof Decls) {
			nodes.append(", shape=Mcircle");
		} else if (node instanceof IntExpression) {
			nodes.append(", shape=pentagon");
		}
		nodes.append("]\n");
		if (node instanceof LeafExpression) {
			leafNodes.add(node);
		}
	}
	
	@Override
	public void visit(NaryFormula formula) {
		ArrayList<Node> rankGroup = new ArrayList<Node>();
		for(Formula child : formula) {
			if (child instanceof ComparisonFormula) {
				ComparisonFormula cf = (ComparisonFormula)child;
				if (cf.left() == cf.right()) continue;
			}
			newEdge(formula, child);
			rankGroup.add(child);
			child.accept(this);
		}
		rankGroups.add(rankGroup);
	}

	@Override
	public void visit(BinaryFormula binFormula) {
		super.visit(binFormula);
		ArrayList<Node> rankGroup = new ArrayList<Node>();
		rankGroup.add(binFormula.left());
		rankGroup.add(binFormula.right());
		rankGroups.add(rankGroup);
	}
	
	@Override
	public void visit(QuantifiedFormula qFormula) {
		newEdge(qFormula, qFormula.formula());
		qFormula.formula().accept(this);
		
		if (qFormula.decls() instanceof Decl) {
			Decl decl = (Decl)qFormula.decls();
			newEdge(qFormula, decl.variable());
			newEdge(decl.variable(), decl.expression());
		} else if (qFormula.decls() instanceof Decls) {
			for (Decl decl : qFormula.decls()) {
				newEdge(qFormula, decl.variable());
				newEdge(decl.variable(), decl.expression());
			}
		}
	}

	@Override
	protected void enter(Node node) {
		// TODO Auto-generated method stub
		
	}

	@Override
	protected void leave(Node node) {
		// TODO Auto-generated method stub
		
	}

	@Override
	protected void newCompound(Node parent, Node child) {
		// TODO Auto-generated method stub
		
	}

	@Override
	protected void newEdge(Node parent, Node child, int pos) {
		// TODO Auto-generated method stub
		
	}

	@Override
	protected boolean visited(Node n) {
		// TODO Auto-generated method stub
		return false;
	}

	
}
